0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 183 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 9 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T24, []), .(T24, [])) → revB_out_ga(.(T24, []), .(T24, []))
revB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1A_in_ggga([], T397, T398, .(T397, T398)) → r1A_out_ggga([], T397, T398, .(T397, T398))
r1A_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, r1A_out_ggga(T410, T409, .(T411, T412), T414)) → r1A_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T24, []), .(T24, [])) → revB_out_ga(.(T24, []), .(T24, []))
revB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1A_in_ggga([], T397, T398, .(T397, T398)) → r1A_out_ggga([], T397, T398, .(T397, T398))
r1A_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, r1A_out_ggga(T410, T409, .(T411, T412), T414)) → r1A_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → R1A_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → U1_GGGA(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → R1A_IN_GGGA(T410, T409, .(T411, T412), T414)
revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T24, []), .(T24, [])) → revB_out_ga(.(T24, []), .(T24, []))
revB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1A_in_ggga([], T397, T398, .(T397, T398)) → r1A_out_ggga([], T397, T398, .(T397, T398))
r1A_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, r1A_out_ggga(T410, T409, .(T411, T412), T414)) → r1A_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → R1A_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → U1_GGGA(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → R1A_IN_GGGA(T410, T409, .(T411, T412), T414)
revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T24, []), .(T24, [])) → revB_out_ga(.(T24, []), .(T24, []))
revB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1A_in_ggga([], T397, T398, .(T397, T398)) → r1A_out_ggga([], T397, T398, .(T397, T398))
r1A_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, r1A_out_ggga(T410, T409, .(T411, T412), T414)) → r1A_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → R1A_IN_GGGA(T410, T409, .(T411, T412), T414)
revB_in_ga([], []) → revB_out_ga([], [])
revB_in_ga(.(T24, []), .(T24, [])) → revB_out_ga(.(T24, []), .(T24, []))
revB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → revB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
revB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → revB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
revB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → revB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
revB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → revB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
revB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → revB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
revB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → revB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
revB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
r1A_in_ggga([], T397, T398, .(T397, T398)) → r1A_out_ggga([], T397, T398, .(T397, T398))
r1A_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, r1A_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, r1A_out_ggga(T410, T409, .(T411, T412), T414)) → r1A_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, r1A_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → revB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
R1A_IN_GGGA(.(T409, T410), T411, T412, T414) → R1A_IN_GGGA(T410, T409, .(T411, T412), T414)
R1A_IN_GGGA(.(T409, T410), T411, T412) → R1A_IN_GGGA(T410, T409, .(T411, T412))
From the DPs we obtained the following set of size-change graphs: